Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(U12(X)) → MARK(X)
U121(mark(X)) → U121(X)
MARK(tt) → ACTIVE(tt)
__1(X1, active(X2)) → __1(X1, X2)
ACTIVE(U11(tt)) → U121(tt)
MARK(U11(X)) → U111(mark(X))
ISNEPAL(mark(X)) → ISNEPAL(X)
MARK(isNePal(X)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(__(X, nil)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
U111(active(X)) → U111(X)
U121(active(X)) → U121(X)
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
ACTIVE(isNePal(__(I, __(P, I)))) → U111(tt)
ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → U121(mark(X))
__1(active(X1), X2) → __1(X1, X2)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → ISNEPAL(mark(X))
ACTIVE(__(__(X, Y), Z)) → __1(X, __(Y, Z))
MARK(__(X1, X2)) → __1(mark(X1), mark(X2))
U111(mark(X)) → U111(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ISNEPAL(active(X)) → ISNEPAL(X)
__1(X1, mark(X2)) → __1(X1, X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(U12(X)) → ACTIVE(U12(mark(X)))
ACTIVE(__(__(X, Y), Z)) → __1(Y, Z)
ACTIVE(U12(tt)) → MARK(tt)
__1(mark(X1), X2) → __1(X1, X2)
MARK(nil) → ACTIVE(nil)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U12(X)) → MARK(X)
U121(mark(X)) → U121(X)
MARK(tt) → ACTIVE(tt)
__1(X1, active(X2)) → __1(X1, X2)
ACTIVE(U11(tt)) → U121(tt)
MARK(U11(X)) → U111(mark(X))
ISNEPAL(mark(X)) → ISNEPAL(X)
MARK(isNePal(X)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(__(X, nil)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
U111(active(X)) → U111(X)
U121(active(X)) → U121(X)
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
ACTIVE(isNePal(__(I, __(P, I)))) → U111(tt)
ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → U121(mark(X))
__1(active(X1), X2) → __1(X1, X2)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → ISNEPAL(mark(X))
ACTIVE(__(__(X, Y), Z)) → __1(X, __(Y, Z))
MARK(__(X1, X2)) → __1(mark(X1), mark(X2))
U111(mark(X)) → U111(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ISNEPAL(active(X)) → ISNEPAL(X)
__1(X1, mark(X2)) → __1(X1, X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(U12(X)) → ACTIVE(U12(mark(X)))
ACTIVE(__(__(X, Y), Z)) → __1(Y, Z)
ACTIVE(U12(tt)) → MARK(tt)
__1(mark(X1), X2) → __1(X1, X2)
MARK(nil) → ACTIVE(nil)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 5 SCCs with 11 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNEPAL(mark(X)) → ISNEPAL(X)
ISNEPAL(active(X)) → ISNEPAL(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ISNEPAL(mark(X)) → ISNEPAL(X)
ISNEPAL(active(X)) → ISNEPAL(X)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 4 + x_1   
POL(mark(x1)) = 4 + (4)x_1   
POL(ISNEPAL(x1)) = (4)x_1   
The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U121(mark(X)) → U121(X)
U121(active(X)) → U121(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U121(mark(X)) → U121(X)
U121(active(X)) → U121(X)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 4 + (4)x_1   
POL(U121(x1)) = (4)x_1   
POL(mark(x1)) = 4 + x_1   
The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U111(active(X)) → U111(X)
U111(mark(X)) → U111(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U111(active(X)) → U111(X)
U111(mark(X)) → U111(X)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 4 + (4)x_1   
POL(U111(x1)) = (4)x_1   
POL(mark(x1)) = 4 + x_1   
The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

__1(X1, active(X2)) → __1(X1, X2)
__1(active(X1), X2) → __1(X1, X2)
__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


__1(X1, active(X2)) → __1(X1, X2)
__1(active(X1), X2) → __1(X1, X2)
__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 4 + (4)x_1   
POL(__1(x1, x2)) = (4)x_1 + x_2   
POL(mark(x1)) = 3 + (4)x_1   
The value of delta used in the strict ordering is 3.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → MARK(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(U12(X)) → ACTIVE(U12(mark(X)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(U12(X)) → ACTIVE(U12(mark(X)))
The remaining pairs can at least be oriented weakly.

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → MARK(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 5/4   
POL(MARK(x1)) = 4   
POL(tt) = 0   
POL(__(x1, x2)) = 1   
POL(U12(x1)) = 0   
POL(mark(x1)) = 4   
POL(U11(x1)) = 1   
POL(isNePal(x1)) = 1   
POL(ACTIVE(x1)) = 3 + x_1   
POL(nil) = 15/4   
The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented:

__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U12(active(X)) → U12(X)
U12(mark(X)) → U12(X)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → MARK(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ACTIVE(isNePal(__(I, __(P, I)))) → MARK(U11(tt))
MARK(isNePal(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = x_1   
POL(MARK(x1)) = (4)x_1   
POL(tt) = 0   
POL(__(x1, x2)) = x_1 + x_2   
POL(U12(x1)) = (3/2)x_1   
POL(mark(x1)) = x_1   
POL(U11(x1)) = (2)x_1   
POL(isNePal(x1)) = 1 + (4)x_1   
POL(ACTIVE(x1)) = (4)x_1   
POL(nil) = 0   
The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented:

active(U11(tt)) → mark(U12(tt))
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
mark(U11(X)) → active(U11(mark(X)))
mark(nil) → active(nil)
active(U12(tt)) → mark(tt)
mark(tt) → active(tt)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U12(active(X)) → U12(X)
U12(mark(X)) → U12(X)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(__(X, nil)) → MARK(X)
MARK(U11(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(isNePal(X)) → ACTIVE(isNePal(mark(X)))
The remaining pairs can at least be oriented weakly.

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(__(X, nil)) → MARK(X)
MARK(U11(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 4 + (2)x_1   
POL(MARK(x1)) = 4   
POL(tt) = 0   
POL(__(x1, x2)) = 4   
POL(U12(x1)) = 1/4 + (15/4)x_1   
POL(mark(x1)) = 0   
POL(U11(x1)) = 4   
POL(isNePal(x1)) = 0   
POL(ACTIVE(x1)) = x_1   
POL(nil) = 0   
The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented:

__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ACTIVE(__(X, nil)) → MARK(X)
ACTIVE(__(nil, X)) → MARK(X)
The remaining pairs can at least be oriented weakly.

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = x_1   
POL(MARK(x1)) = (4)x_1   
POL(tt) = 0   
POL(__(x1, x2)) = (4)x_1 + x_2   
POL(U12(x1)) = x_1   
POL(mark(x1)) = x_1   
POL(U11(x1)) = x_1   
POL(isNePal(x1)) = (3/4)x_1   
POL(ACTIVE(x1)) = (4)x_1   
POL(nil) = 4   
The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented:

active(U11(tt)) → mark(U12(tt))
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
mark(U11(X)) → active(U11(mark(X)))
mark(nil) → active(nil)
active(U12(tt)) → mark(tt)
mark(tt) → active(tt)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U12(active(X)) → U12(X)
U12(mark(X)) → U12(X)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(U11(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


ACTIVE(U11(tt)) → MARK(U12(tt))
MARK(U11(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.

MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → ACTIVE(U11(mark(X)))
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = x_1   
POL(MARK(x1)) = (1/4)x_1   
POL(tt) = 0   
POL(__(x1, x2)) = x_1 + x_2   
POL(U12(x1)) = x_1   
POL(mark(x1)) = x_1   
POL(U11(x1)) = 1/4 + (4)x_1   
POL(isNePal(x1)) = 1/2   
POL(ACTIVE(x1)) = (1/4)x_1   
POL(nil) = 0   
The value of delta used in the strict ordering is 1/16.
The following usable rules [17] were oriented:

active(U11(tt)) → mark(U12(tt))
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
mark(U11(X)) → active(U11(mark(X)))
mark(nil) → active(nil)
active(U12(tt)) → mark(tt)
mark(tt) → active(tt)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U12(active(X)) → U12(X)
U12(mark(X)) → U12(X)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(U11(X)) → ACTIVE(U11(mark(X)))
MARK(__(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(U11(X)) → ACTIVE(U11(mark(X)))
The remaining pairs can at least be oriented weakly.

MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = 5/2   
POL(MARK(x1)) = 1/4   
POL(__(x1, x2)) = 1/2   
POL(tt) = 5/2   
POL(U12(x1)) = 4 + (15/4)x_1   
POL(mark(x1)) = 0   
POL(U11(x1)) = 1/4   
POL(isNePal(x1)) = 4 + (2)x_1   
POL(ACTIVE(x1)) = (1/2)x_1   
POL(nil) = 9/4   
The value of delta used in the strict ordering is 1/8.
The following usable rules [17] were oriented:

__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U12(X)) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X2)
The remaining pairs can at least be oriented weakly.

MARK(U12(X)) → MARK(X)
Used ordering: Polynomial interpretation [25,35]:

POL(active(x1)) = x_1   
POL(MARK(x1)) = 3 + x_1   
POL(__(x1, x2)) = 4 + (4)x_1 + x_2   
POL(tt) = 0   
POL(U12(x1)) = x_1   
POL(mark(x1)) = x_1   
POL(U11(x1)) = 0   
POL(isNePal(x1)) = (4)x_1   
POL(ACTIVE(x1)) = 3/4 + x_1   
POL(nil) = 0   
The value of delta used in the strict ordering is 9/4.
The following usable rules [17] were oriented:

__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
U12(active(X)) → U12(X)
U12(mark(X)) → U12(X)
U11(active(X)) → U11(X)
U11(mark(X)) → U11(X)
active(U11(tt)) → mark(U12(tt))
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
mark(U11(X)) → active(U11(mark(X)))
mark(nil) → active(nil)
isNePal(active(X)) → isNePal(X)
isNePal(mark(X)) → isNePal(X)
active(U12(tt)) → mark(tt)
mark(tt) → active(tt)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
                                      ↳ QDP
                                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U12(X)) → MARK(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(U12(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(MARK(x1)) = (4)x_1   
POL(U12(x1)) = 1 + (4)x_1   
The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
                                      ↳ QDP
                                        ↳ QDPOrderProof
                                          ↳ QDP
                                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(U11(tt)) → mark(U12(tt))
active(U12(tt)) → mark(tt)
active(isNePal(__(I, __(P, I)))) → mark(U11(tt))
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(U11(X)) → active(U11(mark(X)))
mark(tt) → active(tt)
mark(U12(X)) → active(U12(mark(X)))
mark(isNePal(X)) → active(isNePal(mark(X)))
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
U11(mark(X)) → U11(X)
U11(active(X)) → U11(X)
U12(mark(X)) → U12(X)
U12(active(X)) → U12(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.